$\forall$$X$:EventsWithValues\{i\}. EVal{-}atom{-}free\{i:l\}($X$) $\in$ Prop$_{\mbox{\scriptsize i'}}$